$\forall$$A$, $B$:Type, $f$:($A$$\rightarrow$$B$), $L$:($A$ List), $L_{1}$, $L_{2}$:($B$ List).
\\[0ex](map($f$;$L$) = ($L_{1}$ @ $L_{2}$) $\in$ ($B$ List))
\\[0ex]$\Rightarrow$ \{map($f$;firstn($\parallel$$L_{1}$$\parallel$;$L$)) = $L_{1}$ \& map($f$;nth\_tl($\parallel$$L_{1}$$\parallel$;$L$)) = $L_{2}$\}